/*
 * Atomic Predicates for Transformers
 * 
 * Copyright (c) 2015 UNIVERSITY OF TEXAS AUSTIN. All rights reserved. Developed
 * by: HONGKUN YANG and SIMON S. LAM http://www.cs.utexas.edu/users/lam/NRL/
 * 
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * with the Software without restriction, including without limitation the
 * rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
 * sell copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 * 
 * 1. Redistributions of source code must retain the above copyright notice,
 * this list of conditions and the following disclaimers.
 * 
 * 2. Redistributions in binary form must reproduce the above copyright notice,
 * this list of conditions and the following disclaimers in the documentation
 * and/or other materials provided with the distribution.
 * 
 * 3. Neither the name of the UNIVERSITY OF TEXAS AUSTIN nor the names of the
 * developers may be used to endorse or promote products derived from this
 * Software without specific prior written permission.
 * 
 * 4. Any report or paper describing results derived from using any part of this
 * Software must cite the following publication of the developers: Hongkun Yang
 * and Simon S. Lam, Scalable Verification of Networks With Packet Transformers
 * Using Atomic Predicates, IEEE/ACM Transactions on Networking, October 2017,
 * Volume 25, No. 5, pages 2900-2915 (first published as IEEE Early Access
 * Article, July 2017, Digital Object Identifier: 10.1109/TNET.2017.2720172).
 * 
 * 
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * CONTRIBUTORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS WITH
 * THE SOFTWARE.
 */
package transformer;

import java.util.*;

import common.PositionTuple;

public abstract class AbstractState {

    public static final int contflag = 0;
    public static final int destflag = 1;
    public static final int loopflag = 2;
    public static final int deadflag = 3;
    
    AbstractState parent;

    PositionTuple pt;

    // need representation for a packet set

    int flag;
    // nextState == null or is empty if and only if there is no children
    //                         ^^ for the update case
    ArrayList<AbstractState> nextState;
    /*
     * ports have traveled prior to the current position
     */
    HashSet<PositionTuple> ptvisited;
    /*
     * device have traveled prior to the current position
     */
    HashSet<String> dvisited;
    
    /**
     * 
     * @return the size of the tree rooted at
     *         the current node
     */
    public int tree_size()
    {
        int tree_size = 1;
        if(!is_leaf())
        {
            for(AbstractState child : nextState)
            {
                tree_size += child.tree_size();
            }
        }
        
        return tree_size;
    }
    
    public boolean can_be_extended()
    {
        if(flag == loopflag || flag == destflag)
        {
            return false;
        }
        return true;
    }

    public boolean is_leaf()
    {
        return nextState == null || nextState.isEmpty();
    }

    public ArrayList<AbstractState> get_all_descendants()
    {
        ArrayList<AbstractState> descendants = new ArrayList<AbstractState> ();

        get_all_descendants(descendants);

        return descendants;
    }

    private void get_all_descendants(ArrayList<AbstractState> descendants)
    {
        if(is_leaf())
        {
            return;
        }else
        {
            descendants.addAll(nextState);
        }

        for(AbstractState nexts : nextState)
        {
            nexts.get_all_descendants(descendants);
        }
    }


    public AbstractState(PositionTuple pt)
    {
        this.pt = pt;
        dvisited = new HashSet<String>();
        ptvisited = new HashSet<PositionTuple> ();
        flag = deadflag;
        nextState = null;
    }

    public AbstractState(PositionTuple pt,  HashSet<String> visitedset, HashSet<PositionTuple> ptvisitedset)
    {
        this.pt = pt;
        dvisited = visitedset;
        ptvisited = ptvisitedset;
        flag = deadflag;
        nextState = null;
    }


    public PositionTuple getPosition()
    {
        return pt;
    }

    public void addNextState(AbstractState s)
    {
        if(nextState == null)
        {
            nextState = new ArrayList<AbstractState>();
            flag = contflag;
        }
        nextState.add(s);
        s.parent = this;
    }

    public void delNextState(AbstractState s)
    {
        if(nextState != null)
        {
            boolean res = nextState.remove(s);
            if(res)
            {
                s.parent = null;
            }
            //System.out.println(s);
            if(nextState.isEmpty())
            {
                nextState = null;
                flag = deadflag;
            }
        }
    }

    public void delNextState(PositionTuple pt)
    {
        if(nextState == null)
        {
            return;
        }else
        {
            for(int i = nextState.size()-1; i >= 0; i --)
            {
                if(nextState.get(i).getPosition().equals(pt))
                {
                    AbstractState child = nextState.get(i);
                    child.parent = null;
                    
                    nextState.remove(i);
                }
            }
        }
    }
    
    public AbstractState getNextState(PositionTuple pt)
    {
        if(nextState != null)
        {
            for(AbstractState nexts : nextState)
            {
                if(nexts.getPosition().equals(pt))
                {
                    return nexts;
                }
            }
        }
        return null;
    }

    public HashSet<String> getVisited()
    {
        return dvisited;
    }

    public HashSet<PositionTuple> getPtVisited()
    {
        return ptvisited;
    }

    public HashSet<String> getAlreadyVisited()
    {
        HashSet<String> alv = new HashSet<String> (dvisited);
        alv.add(pt.getDeviceName());
        return alv;
    }

    public HashSet<PositionTuple> getPtAlreadyVisited()
    {
        HashSet<PositionTuple> alv = new HashSet<PositionTuple> (ptvisited);
        alv.add(pt);
        return alv;
    }

    public boolean loopDetected()
    {
        if(dvisited.contains(pt.getDeviceName()))
        {
            flag = loopflag;
            return true;
        }else
        {
            return false;
        }
    }

    public static void removeLoop(AbstractState root)
    {
        if(root.nextState != null)
        {
            ArrayList<AbstractState> to_del = new ArrayList<AbstractState> ();
            for(AbstractState s : root.nextState)
            {
                if(s.ptLoopDetected())
                {
                    to_del.add(s);
                }else
                {
                    removeLoop(s);
                }
            }
            for(AbstractState d : to_del)
            {
                root.delNextState(d);
            }

        }
    }

    public boolean ptLoopDetected()
    {
        if(ptvisited.contains(pt))
        {
            flag = loopflag;
            return true;
        }else
        {
            return false;
        }
    }

    public boolean destDetected(PositionTuple destpt)
    {
        if(pt.equals(destpt))
        {
            flag = destflag;
            return true;
        }else
        {
            return false;
        }

    }

    public String printFlag()
    {
        switch (flag) {
        case contflag: 
            return "cont";
        case destflag: 
            return "dest";
        case loopflag:
            return "loop";
        case deadflag:
            return "dead";
        default: 
            System.err.println("unknown flag " + flag);
            System.exit(1);
        }
        return null;
    }

    public abstract String toString();  

    /**
     * depth first print
     */
     public void printState()
    {
        printState_recur("");
    }

    public void printState_recur(String headstr)
    {
        String newheadstr = headstr + toString();
        if(nextState == null)
        {
            System.out.println(newheadstr + printFlag());
        }else
        {
            for(int i = 0; i < nextState.size(); i ++)
            {
                AbstractState nxtS = nextState.get(i);
                nxtS.printState_recur(newheadstr);
            }
        }

    }

    public void printLoop()
    {
        printLoop_recur("");
    }

    public void printLoop_recur(String headstr)
    {
        String newheadstr = headstr + toString();
        if(flag == loopflag)
        {
            System.out.println(newheadstr + printFlag());
            return;
        }else if(nextState == null)
        {
            return;
        }
        else
        {
            for(AbstractState nxtS : nextState)
            {
                nxtS.printLoop_recur(newheadstr);
            }
        }
    }

}
